%
% Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
%
% SPDX-License-Identifier: BSD-2-Clause
%

@InProceedings{Cock08,
  author =       {David Cock},
  title =        {Bitfields and Tagged Unions in {C}: Verification through
                  Automatic Generation},
  booktitle =    {Proc, 5th VERIFY},
  year =         {2008},
  editor =       {Bernhard Beckert and Gerwin Klein},
  series =       {{CEUR} Workshop Proceedings},
  address =      {Sydney, Australia},
  volume =       372,
  month =        aug,
  pages =        {44--55},
  keywords =     {nicta, l4, l4verified},
  format =       {pdf}
}

 @phdthesis{Tuch:phd,
    school           = {School of Computer Science and Engineering},
    author           = {Harvey Tuch},
    title            = {Formal Memory Models for Verifying {C} Systems Code},
    month            = {Aug},
    year             = 2008,
    type             = {{PhD} Thesis},
    address          = {University of NSW, Sydney 2052, Australia}
  }

@inproceedings{Tuch:separation-logic:2007,
  author = {Harvey Tuch and Gerwin Klein and Michael Norrish},
  title = {Types, Bytes, and Separation Logic},
  booktitle = {POPL '07: Proceedings of the 34th annual ACM SIGPLAN-SIGACT
               symposium on Principles of programming languages},
  year = 2007,
  isbn = {1-59593-575-4},
  pages = {97--108},
  location = {Nice, France},
  doi = {http://doi.acm.org/10.1145/1190216.1190234},
  publisher = {ACM Press},
  address = {New York, NY, USA},
}

@PhdThesis{norrish98,
  author =       {Michael Norrish},
  title =        {{C} Formalised in {HOL}},
  school =       {Computer Laboratory, University of Cambridge},
  year =         1998,
  note =         {Also published as Technical Report 453, available from \url{http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-453.pdf}}
}

@InProceedings{Harrison:TPHOLs2005:Euclidean-Space,
  author =       {John Harrison},
  title =        {A {HOL} Theory of {Euclidean} Space},
  crossref =  {tphols2005},
  pages =     {114--129}
}

@Proceedings{tphols2005,
 booktitle =     {Theorem Proving in Higher Order Logics, 18th
                  International Conference},
 title =         {Theorem Proving in Higher Order Logics, 18th
                  International Conference},
  year =         2005,
  editor =       {Joe Hurd and T. Melham},
  series =       {Lecture Notes in Computer Science},
  publisher =    {Springer},
  volume =       3603
}
